The invention relates generally to analyzing message sequence charts (MSCs) and more particularly to model checking systems modeled with high level MSCs.
Message Sequence Charts (MSCs) are commonly used to describe the executions of communication systems. An MSC describes messages passed between the participating concurrent processes in the system, abstracting away details such as program variables and their values. Different system executions or scenarios can be described using MSCs, providing a representation of different system features. Grouping together different scenarios is facilitated using high-level or hierarchical MSCs (HMSCs). These are graphs that include nodes and edges connecting the nodes, where each of the nodes references a single MSC. The graph structure allows for combining together scenarios and for describing execution alternatives according to the branches of the graph. This simple standard is particularly useful for specifying communication protocols.
Because HMSCs do not impose constraints on the number of sent but unreceived messages, HMSCs can describe infinite state spaces. For example, an HMSC can describe a system where a process can send infinite messages without receiving a message from any process in the system. The lack of constraints on sent but received message complicates the automatic verification of MSCs. Standard model checking methods, usually applied to finite state systems, cannot automatically verify an HMSC. For example, checking linear temporal logic (LTL) properties of HMSCs is undecidable. This result is discussed in R. Alur, M. Yannakakis, xe2x80x9cModel Checking of Message Sequence Charts,xe2x80x9d CONCUR""99, Concurrency Theory, LNCS 1664, Eindhoven, The Netherlands, 1999.
Checking LTL properties of HMSCs is based on the linearizations of the HMSCs. Linearizing an HMSC means completing the partial order between the events imposed by the HMSC""s scenarios into total orders. In this approach, all the linearizations of an MSC execution satisfy the given LTL specification. Adding a bound on the number of messages in any communication channel permits translating HMSCs to finite state models that are exponentially larger than the original HMSC description. Standard model checking methods, like checking LTL properties, can then be applied to the finite state model. Besides the complexity problem, which can make this approach impractical to implement, when checking LTL properties, different linearizations of the same MSC execution may not agree on the satisfaction of a given LTL specification.
Another known verification method for HMSCs is based directly on the partial order semantics of HMSCs. Verification according to this method requires specifying properties of HMSCs using HMSCs. Intersecting two HMSCs is analogous to checking the intersection of a system automaton and a specification automaton in the automata-theorectic approach to model checking. Automata-theoretic model checking is discussed in M. Y. Vardi, P. Wolper, xe2x80x9cAn Automata-theoretic Approach To Program Verification,xe2x80x9d Proc. 1st Annual Symposium on Logic in Computer Science IEEE, 1986. In this method, the specification automaton specifies the disallowed executions. This is done to avoid the process of complementation. Unfortunately, the problem of checking HMSC intersections in this method is also undecidable.
Model checking of HMSCs is also discussed in A. Muscholl, D. Peled, Z. Su, xe2x80x9cDeciding Properties for Message Sequence Charts,xe2x80x9d FoSSaCS, Foundations of Software Science and Computation Structures, Lisbon, Portugal, LNCS 1378, 226-423. In the approach to HMSC model checking described therein, the HMSC specifying disallowed executions is given a relaxed interpretation: the HMSC specifies the essential ordering between some events; however, it allows more events and additional ordering to be included in each execution. In essence, this framework amounts to pattern matching between two HMSCs.
In the method according to the principles of the invention, a temporal logic is used to check a property of a system modeled with a causal (partial order) structure, such as a hierarchical message sequence chart (HMSC). The logic is interpreted over the causal structures. One such logic is a subset of xe2x80x9ctemporal logic causalityxe2x80x9d (TLC) and is used to define a specification for the property of interest. This subset of TLC (hereafter xe2x80x9cTLCxe2x88x92xe2x80x9d) provides a logic for expressing specifications that can be automatically translated into a specification automaton. In the method according to the principles of the invention, an implementation automaton is constructed from the causal structure. Property checking then proceeds by checking an intersection of the specification automaton and the implementation automaton for emptiness.
The property checking method according to the principles of the invention can be implemented in a general purpose computer. A memory stores TLCxe2x88x92 specifications, HMSCs, and instructions which, when executed by the computer processor, causes the processor to carry out the method of the invention. In one aspect, the temporal logic specifications are expressed in PROMELA (PROcess MEta LAnguage) code, which is the input language for the SPIN model checking system. When expressed as PROMELA code, the SPIN system causes the computer to use the specification in the model checking method according to the principles of the invention.